
We have introduced \rnd, a high-level Petri net framework to address problems related to toxicogenomics. In \rnd, systems consist of a set of species present in the environment at a given  level. Species can degrade as time passes by and their presence is governed by a  set of rules (reactions). In a reaction, species can have the role of reactants, inhibitors or products. A reaction has a given duration, and it can take place only if all reactants are available and all  inhibitors are not for the whole duration of the reaction. Depending on the type of reaction, products  levels are either increased or decreased. We have shown that properties of biological systems can be expressed in a suitable temporal logic and verified thanks to a sound and complete abstraction defined for \rnd.  
Moreover, we have illustrated our framework  in the modeling of blood glucose regulation. This highlights  the capability  of \rnd to formalize various kinds of regulatory networks:  genetics or  signaling. As a matter of fact, we believe that with few adjustments \rnd  can be adapted to describe also metabolic networks.


% \comment{aggiungere qualcosa sul fatto che il modello non e' limitato as it is a familiar process and it shows that our model is not limited to genetic regulations but it may express other kinds of interactions. }


The main application of our work concerns the verification of properties of systems defined in terms of  rules or reactions. 
From a technical point of view, the closest related work is on reaction systems \cite{DBLP:journals/ijfcs/BrijderEMR11} or their Petri net representation \cite{koutnyreaction}. Also, although we use a similar definition for reactions, the semantics that we have proposed is inherently different: in \cite{DBLP:journals/ijfcs/BrijderEMR11}  all  enabled reactions occur in one step while we consider an interleaving semantics. 
Moreover, we have introduced discrete abstract  levels that, to the best of our knowledge, are not taken into account in reaction systems.
Also, we have presented a more elaborated notion of time that governs both species and reactions. 
In  \cite{DBLP:conf/birthday/BrijderER11}, the authors consider an extension of reaction systems with duration but it concerns only decay and not  duration of reactions. Furthermore the decay is  referred to the number of steps and not to an independent clock. 
In fact, our representation of time is considerably different from the approaches traditionally used in time and timed Petri nets 
(\cite{DBLP:journals/tcs/CeroneM99} presents a survey with insightful comparison of the different approaches).
The main difference lies on the fact that the  progression of time is implicit and  external to the system. By contrast, in our proposal we have assumed the presence of  an explicit  global clock  whose values (timestamps) can be assigned to tokens. 
This is also  different from the notion of timestamps introduced in  \cite{timestamp} that again refers to an implicit notion of time.
Indeed,  our approach is closer to Petri nets with causal time  \cite{DBLP:journals/entcs/ThanhKP02} for the presence of explicit clocks and corresponding update transitions but \rnd networks have a clock which cannot be suspended under the influence of the environment.
 
In a broader sense, our work could also be related to P-systems \cite{DBLP:journals/ijfcs/PaunPRS11,DBLP:journals/fuin/KleijnK11} or the $\kappa$-calculus \cite{DBLP:journals/tcs/DanosL04} that  describe the evolution of cells through rules. 
Both these approaches are mainly oriented to simulation while we are interested in  verification aspects. Finally, always related to the modeling in Petri nets but with a different aim,  levels have been used in qualitative approaches to address problems related to the identification of steady states in genetic networks such as in \cite{DBLP:journals/nc/ChaouiyaNRT11}.  Nevertheless these contributions abstract away from time related aspects that are instead central in our proposal. 

As for future work, one of our main objectives is to build a complete framework for  addressing toxicogenomics problems in the context of the design of synthetic entities. This accounts for building a connection between \rnd and the CAD environment for synthetic biology GUBS \cite{Basso-Blandin2013}. This connection should be easy as the output of GUBS is already a set of reactions. This way, the discovery of toxic behaviors can be exploited to modify the design of the synthetic entity by using different sets of biological components (bio-bricks) which have  equivalent functionalities but do not introduce hazardous behaviors.   

From a more technical point of view, we envisage to introduce a suitable type system that would permit to define well formed systems thus, for instance, allowing to check the consistency of \rnd networks. 
Secondly, we are interested in optimizing the construction of the Kripke structure thus obtaining a lower bound to the number of  states. 
A first direction to explore would be of getting rid of the redundant/unreachable states.
Finally, the model we have presented here, can be extended in several directions. One of such extensions would be to add a notion of space, \ie species can occur simultaneously at different positions.
This extension would  represent the fact that reactions may occur  in different compartments (e.g. RNA polymerase). Notice that this complicates considerably the description of systems, as the same species could appear several time with different expression level and in different locations.
% For instance, one can choose to work with continuous time instead of discrete. This solution would be certainly closer to reality but poses a number of problems as  it has a negative impact on the complexity of the system: indeed, reachability immediately  becomes undecidable.
%
%A effacer
%
%There is an increasing interest in computer science on how to provide tools that should support the development of all the aspects related to synthetic biology: aided design, simulation, and verification \cite{computational}.
%As a matter of fact, there have been introduced a number of CAD environments~\cite{Czar2009,Bilitchenko2011} and programming languages~\cite{Basso-Blandin2012,Beal2011} that are dedicated to  synthetic biology. Independently to  these developments, several models, that span from process algebras, to Petri nets and  from rewriting systems to differential equation, have been proposed to simulate and verify properties of biological systems, for a survey see \cite{pinney,CardelliP09,journals/tcsb/Cardelli05}.


%
%\subsection{related}
%The core of our analysis are pathways. They are reminiscent of rewriting systems and a number of proposals have been introduced to be able to model, simulate and design them. P-systems \cite{DBLP:journals/ijfcs/PaunPRS11,MadhuKrithi} are among the first computing models introduced for this aim, they describe the evolution of cells through rules that are applied in a nondeterministic, maximally parallel way. 
%Similarly the $\kappa$-calculus \cite{DBLP:journals/tcs/DanosL04} describes molecular biology by encoding molecules as graphs and evolution as sets of rewriting rules. 
%
%
%
